feat: `NSMul`/`NPow` type class by JovanGerb · Pull Request #38036 · leanprover-community/mathlib4

JovanGerb · 2026-04-14T10:17:11Z

This PR is adds NSMul, NPow, ZSMul and ZPow classes for the nsmul, npow, zsmul, zpow data fields.

This has a few advantages:

If you first declare a SMul instance, then you don't need to manually write nsmul := (· • ·) and zsmul := (· • ·) . For Pow, the extra benefit is that inferring the instance is preferred over the default field npowRecAuto. So this helps avoid accidental diamonds.
If you first declare a SMul instance on a type synonym, then inferInstanceAs will infer the nsmul field from the SMul instance. This makes it easier to avoid diamonds on type synonyms like Matrix and MonoidAlgebra.
The not-yet-merged instance diamond linter will be able to detect cases where the NSMul and SMul classes do not agree.

In the process of making this PR, I have identified two existing NPow diamonds:

In Mathlib.Algebra.Order.Positive.Field, there were two conflicting NPow instances.
For Fin, there are two conflicting NPow instances. I have overwritten the one in core lean with the one from mathlib that is more computationally efficient.

TODO: the same for QSMul and NNQSMul.

github-actions · 2026-04-14T10:18:17Z

PR summary 044631201f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ NPow
+ NPow.ofPow
+ NPow.toPow
+ NSMul
+ ZPow
+ ZPow.ofPow
+ ZPow.toPow
+ ZSMul
+ instance (n : ℕ) [NeZero n] : HPow (Fin n) ℕ (Fin n)
+ instance (n : ℕ) [NeZero n] : Pow (Fin n) ℕ
+ instance {A : Type*} [SMulZeroClass A R] : SMul A R[M]
- DivInvMonoid.toZPow
- Monoid.toPow
- SubNegMonoid.toZSMul
-++- addGroup

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

Decrease in tech debt: (relative, absolute) = (1.04, 0.03)

Current number	Change	Type
6395	1	backward.isDefEq.respectTransparency
803	-2	backward.privateInPublic
414	-1	backward.privateInPublic.warn
46	-1	dsimp +instances

Current commit 12eaeeacf4
Reference commit 044631201f

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

eric-wieser · 2026-04-14T18:06:40Z

Could you elaborate on the benefit here?

eric-wieser · 2026-04-14T23:18:37Z

If you first declare a SMul instance, then you don't need to manually write nsmul := (· • ·) and zsmul := (· • ·) .

This can also be achieved with [toNatSMul : SMul Nat A] as a field.

JovanGerb · 2026-04-14T23:21:14Z

Sure, but then you lose the ability to write nsmul := ..., and instead you have to write some awkward toNSMul := ⟨...⟩

vihdzp · 2026-04-15T00:22:22Z

+  ⟨fun x n ↦ NPow.npow n x⟩
+
+@[to_additive ofSMul]
+instance NPow.ofPow {M : Type*} [Pow M ℕ] : NPow M := ⟨fun n x ↦ x ^ n⟩


Is this desirable? Shouldn't we just assume that any Pow M ℕ instance already comes from NPow M?

vihdzp · 2026-04-15T00:24:39Z

 @[to_additive] instance addCommMonoid : AddCommMonoid R[M] :=
-  fast_instance% { (inferInstance : AddCommMonoid <| M →₀ R) with
-    nsmul n x := x.mapRange (n • ·) (smul_zero _) }
+  inferInstanceAs <| AddCommMonoid <| M →₀ R


What happened to fast_instance%?

This is the great thing: inferInstanceAs will automatically fill in the nsmul field using the smul that was was declared above. (Recall that inferInstanceAs and fast_instance% do the same kind of instance normalization). Previously, we had to awkwardly declare the nsmul field in order to avoid diamond.

I think this should also answer your other question: yes we do need to infer NSMul instances from SMul instances, for example here.

JovanGerb · 2026-04-15T09:34:56Z

!bench

leanprover-radar · 2026-04-15T09:35:16Z

Benchmark results for 12eaeea against 0446312 are in. There are significant results. @JovanGerb

🟥 build//instructions: +319.8G (+0.19%)

Large changes (1✅, 4🟥)

🟥 build/module/Mathlib.Analysis.CStarAlgebra.Fuglede//instructions: +20.8G (+40.83%)
🟥 build/module/Mathlib.Analysis.SpecialFunctions.Log.Deriv//instructions: +9.1G (+13.23%)
🟥 build/module/Mathlib.CategoryTheory.Triangulated.TriangleShift//instructions: +39.1G (+21.23%)
🟥 build/module/Mathlib.NumberTheory.Harmonic.GammaDeriv//instructions: +8.4G (+23.20%)
✅ build/module/Mathlib.RingTheory.Polynomial.UniversalFactorizationRing//instructions: -47.0G (-16.88%)

Medium changes (16✅, 10🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (39✅, 69🟥)

Too many entries to display here. View the full report on radar instead.

feat: NSMul/NPow type class

bccc247

JovanGerb added the WIP Work in progress label Apr 14, 2026

JovanGerb added 6 commits April 14, 2026 12:42

fix

041b901

use fast instance for Fin exponentiation

0d85eae

clean up that file

e34a60f

do the name for Int

86b4d32

fix

fa54279

fix

65e829c

JovanGerb added 3 commits April 14, 2026 23:21

use smul notation in the Prop fields

febb9c6

progress

ff1b9de

fix test

673fedc

JovanGerb added 2 commits April 15, 2026 01:36

.

a81983d

.

8fed238

vihdzp reviewed Apr 15, 2026

View reviewed changes

fixes

12eaeea

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: `NSMul`/`NPow` type class#38036

feat: `NSMul`/`NPow` type class#38036
JovanGerb wants to merge 13 commits intoleanprover-community:masterfrom
JovanGerb:Jovan-NSMul

JovanGerb commented Apr 14, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Apr 14, 2026 •

edited

Loading

Declarations diff

Uh oh!

eric-wieser commented Apr 14, 2026

Uh oh!

eric-wieser commented Apr 14, 2026

Uh oh!

JovanGerb commented Apr 14, 2026 •

edited

Loading

Uh oh!

vihdzp Apr 15, 2026

Uh oh!

vihdzp Apr 15, 2026

Uh oh!

JovanGerb Apr 15, 2026

Uh oh!

JovanGerb commented Apr 15, 2026

Uh oh!

leanprover-radar commented Apr 15, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

JovanGerb commented Apr 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Apr 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 044631201f

Import changes for modified files

Declarations diff

Uh oh!

eric-wieser commented Apr 14, 2026

Uh oh!

eric-wieser commented Apr 14, 2026

Uh oh!

JovanGerb commented Apr 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

vihdzp Apr 15, 2026

Choose a reason for hiding this comment

Uh oh!

vihdzp Apr 15, 2026

Choose a reason for hiding this comment

Uh oh!

JovanGerb Apr 15, 2026

Choose a reason for hiding this comment

Uh oh!

JovanGerb commented Apr 15, 2026

Uh oh!

leanprover-radar commented Apr 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

JovanGerb commented Apr 14, 2026 •

edited

Loading

github-actions bot commented Apr 14, 2026 •

edited

Loading

JovanGerb commented Apr 14, 2026 •

edited

Loading

leanprover-radar commented Apr 15, 2026 •

edited

Loading